\begin{tabbing}
$\forall$${\it es}$:ES, ${\it Sys}$:AbsInterface(Top), $f$:sys{-}antecedent(${\it es}$;${\it Sys}$), $b$, $e$:E(${\it Sys}$).
\\[0ex]$b$ is $f$$\ast$($e$)
\\[0ex]$\Rightarrow$ ($\neg$(loc($b$) = loc($e$) $\in$ Id))
\\[0ex]$\Rightarrow$ ($\exists$\=${\it e'}$:E(${\it Sys}$)\+
\\[0ex](loc(${\it e'}$) = loc($e$) $\in$ Id \& ${\it e'}$ is $f$$\ast$($e$) \& $b$ is $f$$\ast$(${\it e'}$) \& ($\neg$(loc($f$(${\it e'}$)) = loc(${\it e'}$) $\in$ Id))))
\-
\end{tabbing}